home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / csplit_2.05.4 < prev    next >
Text File  |  1992-04-03  |  3KB  |  129 lines
  1. %%%
  2. %%% version 2.05.1
  3. %%%   initial version
  4. %%%   split horn clauses into horn clauses
  5. %%% version 2.05.4
  6. %%%   saved split clauses as sent_c
  7. %%%
  8. %%% This is the code for clause splitting.
  9. %%%
  10.  
  11. %%%
  12. %%% Split_clauses splits clauses when necessary.
  13. %%%
  14.     split_clauses :-
  15.       clause_splitting(N),
  16.       sent_C(cl(CSize,_,by(C,V,V,V1,_),I,sp(S,_,_),_,_,_,_)),
  17.       length(C,N1),
  18.       N1 > N,
  19.       erase_clause_C(CSize,C,V1),
  20.       split_clause(C,N,Cs),
  21.       assert_split_clause(Cs,I,S),
  22.       print_split_clause(C,Cs),
  23.       fail.
  24.     split_clauses :-
  25.       sentc_to_sentC_z,
  26.       !.
  27.  
  28. %%%
  29. %%% Split_clause splits a single clause.
  30. %%%
  31.     split_clause(C,N,[C]) :-
  32.       length(C,N1),
  33.       N1 =< N,
  34.       !.
  35.     split_clause(C,N,[C3|Cs]) :-
  36.       N1 is N - 1,
  37.       split_clause_1(C,N1,C1,C2),
  38.       common_variables(C1,C2,Xs),
  39.       gensym('cs$',F),
  40.       L=..[F|Xs],
  41.       split_clause_3(C1,C2,L,C3,C4),
  42.       !,
  43.       split_clause(C4,N,Cs).
  44.     split_clause_1(C,N,C1,C2) :-
  45.       split_clause_2(C,N,C1,C2,1),
  46.       !.
  47.     split_clause_2([L|Ls],N,[L],Ls,N).
  48.     split_clause_2([L|Ls],N,[L|C1],C2,N1) :-
  49.       N2 is N1 + 1,
  50.       !,
  51.       split_clause_2(Ls,N,C1,C2,N2).
  52.     split_clause_3(C1,C2,L,[not L|C1],[L|C2]) :-
  53.       split_clause_4(C1),
  54.       !.
  55.     split_clause_3(C1,C2,L,[L|C1],[not L|C2]).
  56.     split_clause_4([not _|Ls]) :-
  57.       !,
  58.       split_clause_4(Ls).
  59.     split_clause_4([_|Ls]) :-
  60.       negclause(Ls),
  61.       !.
  62.  
  63. %%%
  64. %%% Assert_split_clause asserts the clauses obtained from splitting a clause.
  65. %%% Note that none of clauses to be asserted can be a duplicate of an existing
  66. %%% clauses since they contain a unique literal.  Thus, no duplicate checking
  67. %%% is done.
  68. %%%
  69.     assert_split_clause([],_,_).
  70.     assert_split_clause([C|Cs],I,S) :-
  71.       assert_split_clause_1(C,I,S),
  72.       !,
  73.       assert_split_clause(Cs,I,S).
  74.     assert_split_clause_1(C,I,S) :-
  75.       vars_tail(C,V),
  76.       clause_size(C,CSize),
  77.       linearize_term(C,C1,V1,V2),
  78.       vars_literals(C,W),
  79.       compute_V_lits(W,0,NLits),
  80.       set_sr_status(S,C1,Sp,Ds),
  81.       list_of_Ns(C1,0,Dis),
  82.       calculate_priority_clause(C1,Sp,Ds,Pr),
  83.       assert_split_clause_2(Pr),
  84.       assertz(sent_c(cl(CSize,NLits,by(C1,V1,V2,V,W),I,Sp,Ds,0,Dis,Pr))),
  85.       !.
  86.     assert_split_clause_2(Pr) :-
  87.       priority_bound(PrioBound),
  88.       !,
  89.       check_prioritybound(Pr,PrioBound),
  90.       !.
  91.     assert_split_clause_2(_).
  92.  
  93. %%%
  94. %%% Print_split_clause prints the result of splitting a clause.
  95. %%%
  96.     print_split_clause(_,_) :-
  97.       not(outcsplit),
  98.       !.
  99.     print_split_clause(C,Cs) :-
  100.       nl,
  101.       write_line(5,'clause split:'),
  102.       not(not(print_split_clause_1(C,Cs))),
  103.       !.
  104.     print_split_clause_1(C,Cs) :-
  105.       vars_tail(C,V),
  106.       var_list(V),
  107.       write_line(10,'orig:  ',C),
  108.       print_split_clause_2(Cs),
  109.       !.
  110.     print_split_clause_2([C|Cs]) :-
  111.       print_split_clause_4(C),
  112.       !,
  113.       print_split_clause_3(Cs).
  114.     print_split_clause_3([]).
  115.     print_split_clause_3([C|Cs]) :-
  116.       print_split_clause_5(C),
  117.       !,
  118.       print_split_clause_3(Cs).
  119.     print_split_clause_4(C) :-
  120.       vars_tail(C,V),
  121.       var_list(V),
  122.       write_line(10,'split: ',C),
  123.       !.
  124.     print_split_clause_5(C) :-
  125.       vars_tail(C,V),
  126.       var_list(V),
  127.       write_line(10,'     : ',C),
  128.       !.
  129.